FDL - Nuprl Lemma : mu-bound-unique

Nuprl Lemma : mu-bound-unique

b:

, f:(int_seg(0; b)

), x:int_seg(0; b).
((

(f(x)))

(

y:int_seg(0; b). (

(f(y)))

(y = x

)))

(mu(f) = x

)

Definitions x:A. B(x), P Q, P Q, x:A. B(x), t T, prop{i:l}, , int_seg(i; j), guard(T)

Lemmas assert wf, mu-bound-property, int seg wf, bool wf, nat wf, mu-bound